Nuprl Lemma : filter_append
11,40
postcript
pdf
T
:Type,
P
:(
T
),
l1
,
l2
:(
T
List).
sqequal(filter(
P
; append(
l1
;
l2
)); append(filter(
P
;
l1
); filter(
P
;
l2
)))
latex
Definitions
b
,
P
Q
,
True
,
b
,
ff
,
tt
,
if
b
then
t
else
f
fi
,
t
T
,
reduce(
f
;
k
;
as
)
,
Y
,
append(
as
;
bs
)
,
filter(
P
;
l
)
,
x
:
A
.
B
(
x
)
,
P
Q
,
P
Q
,
guard(
T
)
,
P
Q
Lemmas
assert
of
bnot
,
bool
cases
sqequal
,
bool
wf
origin
T:Type, P:(T
), l1,l2:(T List).
T:Type, P:(T), l1,l2:(T List).
b
Q
b
Tx:A. B(x)
Q Q
Q